COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	1. Proving Properties of Computer Programs
C00009 00003	.ss(logic,First order logic)
C00012 ENDMK
C⊗;
1. Proving Properties of Computer Programs

	Debugging a program by testing example data is lengthy, and mistakes
often remain for years.  Since a program is a mathematical object, it is
possible in principle to prove mathematically that a program meets its
specifications and thus eliminate debuggin by testing examples.  Such
a correctness proof involves making precise the specifications the
program is to meet and writing down in a precise way the reason
process followed by the programmer as he wrote the program.  If the
programmer programmed correctly, he presumably knew at the time
why the parts of the program would do what he wanted.

	A proof of correctness might be informal - intended to be read
by the programmer, his colleagues and potential users or customers.
However, part of the concept of proof in mathematical logic is that checking
it is a mechanical process and can be done by a computer program.
Since proofs of programs are likely to be long, since humans are
often inattentive and inclined to wishful thinking, checking proofs
by computer looks attractive.  Moreover, as more ⊗⊗proof procedures⊗
are developed and as artificial intelligence advances, the computer itself
can do more and more of the actual proving.

	Replacing debugging by computer checked correctness proofs
imposes several requirements.

	1. A language for writing the specifications of programs.
A person reading the specifications should be able to decide whether
he would be satisfied with a program that met them.  It looks like
different forms of specification will be appropriate for different
kinds of programs.  The properties of LISP programs we prove in this
book will be mainly partial specifications.  They are properties
we want the program to have and enhance our confidence in the program,
but one would not necessarily be willing to sign a legal contract to
pay money for just any program that met them.

	We mainly study input-output specifications of the functions
computed by LISP programs, and sometimes we can prove that the
specification completely characterize the function.  Sometimes
operational specifications, such as the time or memory required,
and be translated into functional specifications of ⊗⊗derived program⊗.

	2. The proof language must admit assertions that correspond
to what the programmer wants to say about the parts of his program,
what they do, and how they fit together.

	3. The proof steps must correspond to the programmer's
reasoning steps.

	4. Programmers must develop skill in proving programs
along with their skill in writing them.  Programming language
design should avoid anomalies that force unnecessary special
cases in proofs.

	Program proving isn't yet routinely practical for
large programs, but some acquaintance with program proving
is important for every computer scientist and educated programmer
if only because it will make his informal reasoning about programs
and their specifications more precise.

	Recursive LISP programs are especially suited for
correctness proofs, because they translate directly
into sentences of mathematical logic.  This was an original design
goal of LISP, and some proof techniques were included in the
original course notes on which this book was based.  However,
R.S. Cartwrights 1976 thesis gave the first satisfactory way
of expressing in ordinary first order logic programs not known
in advance to always terminate.

	In this chapter we explain how to prove that pure clean
recursive LISP programs meet functional specifications.  We
concentrate on 

	This chapter describes how to prove that pure clean recursive
LISP programs meet functional specifications.  In order to concentrate
on techniques for proving programs, we will not give proofs of the metatheorems
on which the techniques are based.  Our model here is a calculus
text rather than a treatise on functions of a real variable.

	Subsequent sections of this chapter treat
first order logic,
the first order theory of S-expressions and lists,
representing programs known to terminate and proving their properties,
representing programs not known in advance to terminate and proving
their properties including termination and non-termination,
advanced techniques of mathematical induction
.ss(logic,First order logic)


	First order logic can be used for expressing theories about any
subject matter and for proving that new sentences follow from old ones.
For a full exposition we recommend a course or a text in mathematical
logic, but the following informal introduction should suffice for
understanding our program proofs.

	We illustrate with a simple theory of kinship.

	Suppose we have a domain that includes all humans.  It may
include other things as well such as rocks or numbers, but we don't
care to say.  To distinguish the humans, we have a ⊗predicate called
⊗⊗ishuman⊗ and we write ⊗⊗ishuman(x)⊗ to say that ⊗x is human.
Every human has a father and fathers are male, so we have a function
⊗father, and the father of ⊗x is written ⊗father(x).  To say that
⊗x is male we write ⊗ismale(x).  The letter ⊗x is called a variable,
and it is regarded as ranging over all objects, not only humans.
Thus we can have

⊗⊗Henry = father(Elizabeth)⊗.

	To say that the father of a human is
always human and male, we write

⊗⊗∀x:(ishuman(x) ⊃ ishuman(father(x)) ∧ ismale(father(x)))⊗,

and we now explain the three new symbols ∀ ⊃ and ∧ introduced in
the above sentence.

	⊗⊗∀x:⊗ is read "for all ⊗⊗x⊗", and it means that what follows
is asserted for all elements of the domain.

	⊃ is read "implies", and it means the sentence following
the ⊃ is true if the sentence preceding ⊃ is true.

	∧ is read "and", and it means that both the sentences it
connects are both true.

	Besides the symbols ∀, ⊃ and ∧, we use four more.